$\forall$$T$:Type, $w$:World. \\[0ex]FairFifo $\Rightarrow$ ($\forall$$e$:E, $x$:Id. vartype(loc($e$);$x$) $\subseteq\rho$ $T$ $\Rightarrow$ state\_after($e$).$x$ $=$ ($x$ after $e$) $\in$ $T$)